A, V:Type, f:a:A fp :V  Top, eq:EqDecider(A), x:A. (x  dom(f))  (x  fpf-domain(f)) 

latex

Definitions	(x  l), P  Q, P  Q, P & Q, P  Q, x:A. B(x), t  T, deq-member(eq;x;L), b, Type, , x:AB(x), x:A  B(x), fpf-domain(f), x  dom(f), a:A fp B(a), Top, x. t(x), EqDecider(T)
Lemmas	deq wf, fpf wf, top wf, iff functionality wrt iff, assert-deq-member, assert wf, deq-member wf, l member wf